Nuprl Lemma : ideal_defines_eqv
13,42
postcript
pdf
r
:CRng,
a
:(|
r
|
).
a
Ideal of
r
EquivRel(|
r
|;
u
,
v
.
a
(
u
+
r
(-
r
(
v
))))
latex
Up
rings
1
origin
r:CRng, a:(|r|
). a Ideal of r 
EquivRel(|r|;u,v.a(u +r (-r(v)))) r:CRng, a:(|r|). a Ideal of r EquivRel(|r|;u,v.a(u +r (-r(v))))